compare .tex
File #1: acoiJA.tex
File #2: atoi.tex

Nonmatching lines (File "acoiJA.tex"; Line 192; File "atoi.tex"; Line 192:193)
 192	\title{An Abstract Concept of Optimal Implementation}

 192	\title{An Abstract Concept of Optimal Implementation\\
 193	(Extended Abstract)}


Nonmatching lines (File "acoiJA.tex"; Line 198; File "atoi.tex"; Line 199)
 198	\john{http not Http} http://www.sys.uea.ac.uk/\~{}zurab.}

 199	Http://www.sys.uea.ac.uk/\~{}zurab.}


Nonmatching lines (File "acoiJA.tex"; Line 206; File "atoi.tex"; Line 207)
 206	was also supported by a Dutch NWO grant during his \john{visit to} Vrije

 207	was also supported by a Dutch NWO grant during his working visit at Vrije


Nonmatching lines (File "acoiJA.tex"; Line 218:219; File "atoi.tex"; Line 219)
 218	\john{Extended Abstract at 18pp?} In a previous paper,
 219	we introduced \emph{Stable Deterministic Residual

 219	\zurab{In a previous paper, we introduced \emph{Stable Deterministic Residual


Nonmatching lines (File "acoiJA.tex"; Line 222:234; File "atoi.tex"; Line 222:233)
 222	systems, and \emph{Deterministic Family Structures} (DFSs), which \john{add}
 223	an axiomatized notion of \emph{redex-family} to capture known
 224	\emph{sharing} concepts in the \lc\ and other orthogonal rewrite systems.
 225	In this paper, we introduce and study a concept of
 226	\john{Just say optimal} \emph{optimal
 227	implementation} of DFSs. We show that for any DFS $\cal F$, its
 228	implementation ${\cal F}_I$ is a non-duplicating DFSs with zig-zag as the
 229	family relation, \john{where} Zig-zag is simply the symmetric and transitive closure of
 230	the residual relation on redexes with histories. Further, we show that
 231	sharing is compositional: the sharing in a DFS $\calF$ can be decomposed
 232	into a weaker sharing $\calF'$ (\john{such as} zig-zag) and a sharing in the
 233	implementation $\calF'_I$ of $\calF'$. These results require study of the
 234	family relation in non-duplicating \john{SDRSs}. We show that zig-zag forms a

 222	systems, and \emph{Deterministic Family Structures} (DFSs), which are SDRSs
 223	with an axiomatized notion of \emph{redex-family} to capture known
 224	\emph{sharing} concepts in the \lc\ and other orthogonal rewrite systems.
 225	In this paper, we introduce and study a concept of \emph{(optimal)
 226	implementation} of DFSs. We show that for any DFS $\cal F$, its
 227	implementation ${\cal F}_I$ is a non-duplicating DFSs with zig-zag as the
 228	family relation. (Zig-zag is simply the symmetric and transitive closure of
 229	the residual relation on redexes with histories.) Further, we show that
 230	sharing is compositional: the sharing in a DFS $\calF$ can be decomposed
 231	into a weaker sharing $\calF'$ (for example, zig-zag) and a sharing in the
 232	implementation $\calF'_I$ of $\calF'$. These results require study of the
 233	family relation in non-duplicating DRSs. We show that zig-zag forms a


Nonmatching lines (File "acoiJA.tex"; Line 239; File "atoi.tex"; Line 238)
 239	defined via zig-zag and via extraction yield the same relation.

 238	defined via zig-zag and via extraction yield the same relation.}


Nonmatching lines (File "acoiJA.tex"; Line 255:257; File "atoi.tex"; Line 254:255)
 255	contraction of a single \john{graph} redex~\cite{[levy],[le80]}.
 256	There was no other way
 257	\john{as} Barendregt et al~\cite{[BBKV]} showed that there does not exist a

 254	contraction of a single redex~\cite{[levy],[le80]}.  There was no other way
 255	-- Barendregt et al~\cite{[BBKV]} showed that there does not exist a


Nonmatching lines (File "acoiJA.tex"; Line 264; File "atoi.tex"; Line 262)
 264	optimality theory, and Gonthier's implementation \john{omit:of it}, to Interaction

 262	optimality theory, and Gonthier's implementation of it, to Interaction


Nonmatching lines (File "acoiJA.tex"; Line 298:302; File "atoi.tex"; Line 296:299)
 298	\john{a} concept of
 299	labelling for orthogonal Combinatory Reduction Systems (CRSs), improving
 300	Klop's original labelling system for CRSs~\cite{[Kl.CRS]},
 301	which \john{covers}
 302	orthogonal TRSs and Interaction Systems. \john{Their} labelling is different

 296	their concept of
 297	labelling for orthogonal Combinatory Reduction Systems (CRSs), improving
 298	Klop's original labelling system for CRSs~\cite{[Kl.CRS]}, which cover
 299	orthogonal TRSs and Interaction Systems, and their labelling is different


Nonmatching lines (File "acoiJA.tex"; Line 315:319; File "atoi.tex"; Line 312:315)
 315	optimality results. Such structures were \john{omit:indeed} introduced by the
 316	authors in~\cite{[rndrs]} as \emph{Deterministic Family
 317	Structures} (DFSs) \john{building on} recent developments of
 318	abstract reduction systems with \john{an} axiomatized residual relation,
 319	such as the

 312	optimality results. Such structures were indeed introduced by the
 313	authors in~\cite{[rndrs]} as \emph{Deterministic Family
 314	Structures} (DFSs). This became possible also due to recent developments of
 315	abstract reduction systems with axiomatized residual relation, such as the


Nonmatching lines (File "acoiJA.tex"; Line 327; File "atoi.tex"; Line 323)
 327	residual relation can be duplicating in DRSs \john{and,} unlike ARSs, there is no

 323	residual relation can be duplicating in DRSs, and unlike ARSs, there is no


Nonmatching lines (File "acoiJA.tex"; Line 332:335; File "atoi.tex"; Line 328)
 332	\john{cut out some ()}
 333	\emph{regular stable sets} of `partial results';
 334	\john{maybe intermediate would be clearer than partial}
 335	all interesting sets

 328	\emph{(regular) stable sets} of `(partial) results'; all interesting sets


Nonmatching lines (File "acoiJA.tex"; Line 345:356; File "atoi.tex"; Line 338:344)
 345	In this paper, we continue \john{the} abstract study
 346	of \john{omit:the} optimality
 347	theory started in~\cite{[rndrs]}. We introduce an abstract concept of
 348	\john{is the word optimal important? I assume a range of implementation
 349	with optimal as the goal.}
 350	\emph{optimal implementation}: \john{With} a DFS $\cal F$ we associate a
 351	\emph{non-duplicating} DRS $\calR_I$, called the implementation of $\cal
 352	F$, whose steps exactly correspond to complete family-reduction steps in
 353	$\cal F$, thus \john{,for example,} they model sharing-graph implementation
 354	of L\'evy's complete
 355	family-reductions \john{in the \lc}. It is not difficult to show that
 356	needed reductions in

 338	\zurab{In this paper, we continue our abstract study of the optimality
 339	theory started in~\cite{[rndrs]}. We introduce an abstract concept of
 340	\emph{optimal implementation}: To a DFS $\cal F$ we associate a
 341	\emph{non-duplicating} DRS $\calR_I$, called the implementation of $\cal
 342	F$, whose steps exactly correspond to complete family-reduction steps in
 343	$\cal F$, thus they model sharing-graph implementation of L\'evy's complete
 344	family-reductions. It is not difficult to show that needed reductions in


Nonmatching lines (File "acoiJA.tex"; Line 368:376; File "atoi.tex"; Line 356:362)
 368	sharing in non-duplicating SDRSs \john{omit: in general}. However,
 369	this is not the case
 370	\john{as} the
 371	example of Asperti and Laneve~\cite{[AL]} demonstrating `inadequacy' of
 372	L\'evy's extraction algorithm for Interaction Systems is\john{, when considered
 373	as an Abstract Reduction System,} a non-duplicating SDRS.  This example also
 374	shows that zig-zag does not coincide with the labelling and
 375	their extraction families \john{based on the \emph{shift} operation}.
 376	These effects are

 356	sharing in non-duplicating SDRSs in general. However, this is not the case
 357	-- the
 358	example of Asperti and Laneve~\cite{[AL]} demonstrating `inadequacy' of
 359	L\'evy's extraction algorithm for Interaction Systems is (when considered
 360	as an Abstract Reduction System) a non-duplicating SDRS.  This example also
 361	shows that zig-zag does not coincide with the labelling and their (i.e.,
 362	with the \emph{shift} operation) extraction families. These effects are


Nonmatching lines (File "acoiJA.tex"; Line 381:382; File "atoi.tex"; Line 367)
 381	X)\ar [\mu(\lambda x. X)/x]X$
 382	\john{acceptable to omit:(in a slightly simplified notation),}

 367	X)\ar [\mu(\lambda x. X)/x]X$ (in a slightly simplified notation),


Nonmatching lines (File "acoiJA.tex"; Line 388; File "atoi.tex"; Line 373)
 388	\john{as discussed in} section~\ref{S.zi.ext.}.

 373	(see discussion in section~\ref{S.zi.ext.}).


Nonmatching lines (File "acoiJA.tex"; Line 403:405; File "atoi.tex"; Line 388)
 403	standardization.
 404	\john{The footnote appears in other papers, doesn't it? If so, omit it.}
 405	\footnote{Actually, the extraction process was claimed to

 388	standardization. \footnote{Actually, the extraction process was claimed to


Extra lines in 2nd before 423 in 1st (File "acoiJA.tex"; Line 423; File "atoi.tex"; Line 406)
 406	}


Nonmatching lines (File "acoiJA.tex"; Line 783; File "atoi.tex"; Line 767)
 783	Despite its generality, our family concept does not cover all

 767	\zurab{Despite its generality, our family concept does not cover all


Nonmatching lines (File "acoiJA.tex"; Line 790; File "atoi.tex"; Line 774)
 790	fib(succ^2(0))+fib(succ^1(0))+fib(succ^2(0))\ar\ldots$$ In the Jungle Graph

 774	fib(succ^2(0))+fib(succ(0))+fib(succ^2(0))\ar\ldots$$ In the Jungle Graph


Extra lines in 1st before 781 in 2nd (File "acoiJA.tex"; Line 797; File "atoi.tex"; Line 781)
 797	\john{used $succ^1(0)$ as it is a bit more informative!}


Extra lines in 2nd before 803 in 1st (File "acoiJA.tex"; Line 803; File "atoi.tex"; Line 786)
 786	}


Nonmatching lines (File "acoiJA.tex"; Line 892:896; File "atoi.tex"; Line 876:879)
 892	The `problem' arises because a redex can
 893	\john{adds nothing so omit:(in general)} create a number of
 894	redexes `intuitively' in the same family without \john{the} help of
 895	\john{previous} steps, something which cannot happen in the \lc\
 896	or \john{omit:in} term rewriting.  That these redexes are intuitively in the same

 876	The `problem' arises because a redex can (in general) create a number of
 877	redexes `intuitively' in the same family \zurab{without a help of other
 878	(previous) steps,} something which cannot happen in the \lc\
 879	or in term rewriting.  That these redexes are intuitively in the same


Extra lines in 1st before 897 in 2nd (File "acoiJA.tex"; Line 914:919; File "atoi.tex"; Line 897)
 914	\john{No paragraph break needed.}
 915	Since we want to define an extraction procedure adequate \john{for} zig-zag,
 916	we do not need an operation modelling \emph{shift}\john{added emph}.
 917	Our results in
 918	Section~\ref{S.impl.drs.} will shed further light on the separability
 919	problem.


Extra lines in 2nd before 923 in 1st (File "acoiJA.tex"; Line 923; File "atoi.tex"; Line 900:906)
 900	\zurab{Since we want to define an extraction procedure adequate to zig-zag,
 901	we do not need an operation modelling shift. Our results in
 902	Section~\ref{S.impl.drs.} will shed further light on the separability
 903	problem.}
 904	
 905	
 906	


Nonmatching lines (File "acoiJA.tex"; Line 1539:1540; File "atoi.tex"; Line 1523)
1539	$\bullet$ the \john{arcs?}
1540	branches of the reduction graph of the underlying ARS $A$ of

1523	$\bullet$ the branches of the reduction graph of the underlying ARS $A$ of


Extra lines in 1st before 1528 in 2nd (File "acoiJA.tex"; Line 1545:1554; File "atoi.tex"; Line 1528)
1545	\john{What does starting from $\emp$ mean? That we start from all terms
1546	in which all redexes are in separate families? And then explore all family
1547	reductions?}
1548	
1549	\john{The redexes of the implementation are elements of the powerset of
1550	the redexes of the underlying ARS correspionding to equivalence classes
1551	under the family relation? I think the resdiual relation just carries
1552	over.}
1553	
1554	


Nonmatching lines (File "acoiJA.tex"; Line 1562:1563; File "atoi.tex"; Line 1535:1536)
1562	($PU\fami_I QV$ iff for any $u\in U, v\in V$, $Fam(Pu)=Fam(Qv)$ in
1563	$\calF$; and $Fam(PU)\contr_I Fam(QV)$ iff $Fam(Pu)\contr Fam(Qv)$).

1535	\zurab{($PU\fami_I QV$ iff for any $u\in U, v\in V$, $Fam(Pu)=Fam(Qv)$ in
1536	$\calF$; and $Fam(PU)\contr_I Fam(QV)$ iff $Fam(Pu)\contr Fam(Qv)$)}.


Nonmatching lines (File "acoiJA.tex"; Line 1569:1571; File "atoi.tex"; Line 1542:1543)
1569	in two different families in a term $s$ and $s\red{U}o$, then $V/U$
1570	\john{also} forms a
1571	complete family, \john{omit:too,} in $o$.

1542	in two different families in a term $s$ and $s\red{U}o$, then $V/U$ forms a
1543	complete family too, in $o$.


Nonmatching lines (File "acoiJA.tex"; Line 1575:1576; File "atoi.tex"; Line 1547)
1575	Let $P:t\doar s$ be a \cfr\ in a \john{not defined. means implementation?}
1576	comma DFS ${\cal F}_t=(R_t,\fami,\contr)$,

1547	Let $P:t\doar s$ be a \cfr\ in a comma DFS ${\cal F}_t=(R_t,\fami,\contr)$,


Nonmatching lines (File "acoiJA.tex"; Line 1636:1637; File "atoi.tex"; Line 1607:1608)
1636	$\cal F$. Hence $\lin{{\cal F}}$ is indeed a DFS as it clearly
1637	contains the zig-zag relation. Note that $\lin{{\cal F}}$ is separable as

1607	$\cal F$. Hence $\lin{{\cal F}}$ is indeed a DFS \zurab{as it clearly
1608	contains the zig-zag relation}. Note that $\lin{{\cal F}}$ is separable as


Extra lines in 1st before 1655 in 2nd (File "acoiJA.tex"; Line 1684:1693; File "atoi.tex"; Line 1655)
1684	\john{Does a partial implementation have as steps complete developments of
1685	a subset of redexes from the same family? And complete has complete
1686	developments of a whole family? Obviously there is a continuum from the
1687	original structure to the optimal (complete) implementation. My question
1688	is whether we keep implementation for optimal implementation or allow the
1689	weaker concept. For example, term graph rewriting will (I believe)
1690	sometimes contract multiple redexes from one family (when viewed as an
1691	implementation of an underlying TRS), but does not always contract
1692	complete families. (Well maybe it does in TRS, but not in \lc)}
1693	


Nonmatching lines (File "acoiJA.tex"; Line 1706; File "atoi.tex"; Line 1667)
1706	from~\cite{[rndrs]}\john{:}

1667	from~\cite{[rndrs]}.


Nonmatching lines (File "acoiJA.tex"; Line 1801:1805; File "atoi.tex"; Line 1762:1764)
1801	systems (such as the one in~\cite{[AL]}). This makes \john{clear the}
1802	importance of the
1803	comprehensive investigation of affine families undertaken in this paper.
1804	\john{omit:more transparent.}
1805	As for zig-zag, we have demonstrated in~\cite{[rndrs]}

1762	systems (such as the one in~\cite{[AL]}). This makes importance of the
1763	comprehensive investigation of affine families undertaken in this paper
1764	more transparent. As for zig-zag, we have demonstrated in~\cite{[rndrs]}


Nonmatching lines (File "acoiJA.tex"; Line 2112:2115; File "atoi.tex"; Line 2071:2073)
2112	\section*{Appendix~A}
2113	
2114	\john{note: section* here and for Appendix B}
2115	

2071	\section{Appendix~A}
2072	
2073	


Nonmatching lines (File "acoiJA.tex"; Line 2133:2134; File "atoi.tex"; Line 2091)
2133	standard variant $P'_1$ of $P_1$; then if $u_0$ still creates the
2134	\john{first} step

2091	standard variant $P'_1$ of $P_1$; then if $u_0$ still creates the fist step


Nonmatching lines (File "acoiJA.tex"; Line 2197; File "atoi.tex"; Line 2154)
2197	\section*{Appendix~B: Proof of \Lr{L.mov.red.cre.}}

2154	\section{Appendix~B: Proof of \Lr{L.mov.red.cre.}}


*** EOF on both files at the same time ***
